| Definitions |  x:A. B(x), P & Q, P   Q,  x:A. B(x), Prop, t  T,   x. t(x), S  T, P  Q, P Q, ecl-trans-normal(x), ecl-trans(x), let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), ecl-base-tuple(k;test), p  q, if b t else f fi,  ,  A,  b, sorted(L), false, False, A & B, A B, ecl-trans-halt2(ds;da;A), ecl-trans-h(v), Top, SQType(T), {T}, ecl-trans-type(A), 1of(t), true, ecl-trans-state-from(v;z;L), p  q, list_accum(x,a.f(x;a);y;l), deq-member(eq;x;L), Y, reduce(f;k;as), x,y. t(x;y), Valtype(da;k), event-info(ds;da), ecl-halt(ds;da;x), let x,y,z = a in t(x;y;z), True, xL. P(x), P Q, ecl-act(ds;da;m;x), ecl-trans-es(v), combine-ecl-tuples(A;B;f;g), l1 l2, 2of(t),  T, ecl-trans-state(v;L), ecl-trans-init(v), ecl-trans-ks(v), ecl-trans-a(v), ||as||, isl(x), outl(x), combine-ecl-tuples2(A;B;f;g), i j < k, {i..j }, (x l),  , (xL.P(x)), i j, reset-ecl-tuple(A), ecl-trans-tuple{i:l}(ds;da), ecl-trans-act(ds;da;A), l1 || l2, add-ecl-act(A;m), ecl-add-throw(A;m), ecl-add-catch(A;l), list-diff(eq;as;bs), x(s),  , Unit, x(s1,s2), Dec(P), null(as), as @ bs, hd(l), tl(l), a = b,  |
| Lemmas | ecl-induction, event-info wf, ecl-trans-normal wf, ecl-trans wf, nat plus wf, ecl-trans-halt2 wf, nat plus inc, l member wf, nat wf, ecl-trans-es wf, iff wf, iseg wf, ecl-halt wf, ecl-act wf, ecl-trans-act wf, ecl wf, fpf wf, Knd wf, Id wf, decidable equal bool, le wf, finite-type-bool, select wf, length wf2, int seg wf, no repeats nil, ecl-trans-state wf, ecl-trans-type wf, implies functionality wrt iff, assert wf, band wf, eq int wf, false wf, iff transitivity, assert of band, and functionality wrt iff, assert of eq int, ecl-trans-state-append, top wf, bool sq, btrue wf, subtype rel self, length wf1, non neg length, eq knd wf, eqtt to assert, assert-eq-knd, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, member wf, last induction, ecl-trans-h wf, eclbase wf, ecl-trans-state-from wf, list accum append, bool wf, Knd sq, first-iseg, decidable assert, null wf3, last lemma, last wf, ma-valtype wf, append wf, fpf-cap wf, Kind-deq wf, l all wf, bor wf, iseg append0, length-append, ecl-base-tuple wf, nil member, l all append, assert of bor, or functionality wrt iff, l all cons, l all nil, ecl-trans-tuple wf, combine-ecl-tuples wf, lt int wf, all functionality wrt iff, iff functionality wrt iff, ecl-normal-combine, bfalse wf, assert of lt int, member-merge, combine-ecl-trans-state1, ecl-halt-unique, common iseg compat, iseg transitivity, combine-ecl-trans-state0, true wf, squash wf, decidable functionality, pi1 wf, pi2 wf, append iseg, iseg weakening, ecl-trans-act-nil, decl-state wf, ecl-trans-ks wf, ecl-trans-a wf, ecl-trans-act-last, append is nil, ecl-halt-nil, member append, ecl-act-halt, iseg antisymmetry, iseg append, deq-member wf, assert-deq-member, append assoc, append-cancellation-right, append-cancellation, cons one one, append-impossible, ifthenelse wf, unit wf, combine-ecl-trans-state2, combine-ecl-tuples2 wf, ecl-normal-combine2, it wf, decidable int equal, decidable lt, reduce wf, l exists wf, l exists reduce, append-impossible2, iseg append single, nat properties, ge wf, bool cases, reset-ecl-tuple wf, ecl-reset-halt, star-append-iff, star-append wf, iseg length, assert of null, decidable false, ecl-trans-act functionality, length append, ecl-reset-init, append nil sq, ecl-trans-act-functionality2, general-append-cancellation, hd wf, tl wf, ecl-trans-init wf, ecl-reset-state, ecl-reset-lemma, add-ecl-act wf, iseg-transition-lemma, list accum wf, s-insert-sorted, s-insert-no-repeats, ecl-trans-halt2-add-throw, ecl-add-throw wf, member-s-insert, nat-deq wf, sorted-filter, no repeats filter, ecl-add-catch wf, member-list-diff, ecl-trans-halt2-add-catch |
Type, da:k:Knd fp